\section{Discussion}
\label{s:discussion}

We have shown so far how immutability support can be extended from
non-transitive read-only references (e.g. \Cconst{} or \texttt{final}) to
transitive read-only references (Javari) and further to object immutability
(OIGJ and \Joe) with ownership-like features. A number of interesting
observations deserve further discussion, including initialization of
immutable objects and covariant subtyping in the presence of immutability
information as presented below. We also discuss type states and unique
references with fractional permissions as further extensions that can
complement immutability.




\subsection{Covariant subtyping}

Covariant subtyping allows type arguments to covariantly change in a
type-safe manner.  Variant parametric types~\cite{1152650} attach a
variance annotation to a type argument, e.g.,
\code{Vector\hgn{+Number}} (for covariant typing) or
\code{Vector\hgn{-Number}} (for contravariant typing).

Its subtype relation contains this chain:

\begin{algorithmic}
\STATE $\code{Vector\hgn{Integer}} \st \code{Vector\hgn{+Integer}} \st \code{Vector\hgn{+Number}} \st \code{Vector\hgn{+Object}}$
\end{algorithmic}
The type checker prohibits calling~\code{someMethod(X)} when the
receiver is of type \code{Foo\hgn{+X}}.  For instance, suppose there
is a method \code{isIn(X)} in class~\code{Vector\hgn{X}}.  Then, it is
prohibited to call \code{isIn(Number)} on a reference of type
\code{Vector\hgn{+Number}}.

Java's wildcards have a similar chain in the subtype relation:

\begin{algorithmic}
\STATE $\code{Vector\hgn{Integer}} \st \code{Vector\hgn{?~extends~Integer}}$
\STATE ~$\st\code{Vector\hgn{?~extends~Number}} \st \code{Vector\hgn{?~extends~Object}}$
\end{algorithmic}
Java's wildcards and variant parametric types are different in the
legality of invoking \code{isIn(?~extends~Number)} on a reference of
type \code{Vector\hgn{?~extends~Number}}.  A variant parametric type
system prohibits such an invocation.  Java permits such an invocation,
but the only value of type~\code{?~extends~Number} is \code{null}.

IGJ also contains a similar chain:

\begin{algorithmic}
\STATE $\code{Vector\hgn{Mutable,Integer}} \st \code{Vector\hgn{ReadOnly,Integer}}$
\STATE ~$\st\code{Vector\hgn{ReadOnly,Number}} \st \code{Vector\hgn{ReadOnly,Object}}$
\end{algorithmic}
The restriction on method calls in IGJ is based on user-chosen
\emph{semantics} (whether the method is readonly or not) rather than
on \emph{method signature} as in wildcards and variant parametric
types.  For example, IGJ allows calling \code{isIn(Number)} on a
reference of type \code{Vector\hgn{\ReadOnly,Number}} iff \code{isIn}
is readonly.  IGJ is still type-safe because of the fact that
\code{isIn} is readonly and the restriction on method overriding~\cite{zibin:2007:immutability}.


\subsection{Typestates for objects}

In a typestate system, each object is in a certain state, and the set
of applicable methods depends on the current state.  Verifying
typestates statically is challenging due to the existence of aliases,
i.e., a state-change in a particular object must affect all its
aliases.  Typestates for objects~\cite{deline04typestates} describes a
system called Fugue that
uses linear types to manage
aliasing.

Object immutability can be partially expressed using typestates: by
using two states (mutable and immutable) and declaring that mutating
methods are applicable only in the mutable state.  An additional
method should mark the transition from a mutable state to an immutable
state, and it should be called after the initialization of the object
has finished.  It remains to be seen if systems such
as~\cite{deline04typestates} can handle arbitrary aliases that occur
in real programs, e.g., \code{this} references that escape the
constructor.


\subsection{Fractional Permissions} \label{sec:frac_perm}

The example in Figure~\ref{fig:reader-writer} shows that a
read-only reference to an object does not preclude the existence
of mutable references to the same object elsewhere in the system.
This allows observational exposure --- for good and evil.  The
immutability annotation `\JoeImmutable{}' imposes all the
restrictions a read-only type has, but it also guarantees that no
aliases with write permission exist in the system. \Joe's simple
way of creating an immutable object is to move a \emph{unique}
reference into a variable with immutable type, just as in SafeJava
\cite{boyapati-thesis}. This allows \Joe to encode fractional
permissions using a borrowing construct and do staged construction
of immutables.
%
\begin{figure}[t]
\begin{small}
\begin{java}
class Client {
  <p* inside world> void m1(p:Object obj) {
    obj.mutate(); // Error
    obj.toString(); // Ok
    // assign to field is not possible
  }
  <p- inside world> void m2(p:Object obj) {
    obj.mutate(); // Error
    obj.toString(); // Ok
  }
}
class Fractional<o+ outside owner> {
  unique[this]:Object obj = new this:Object();
  void example(o:Client c)  {
    borrow obj as p*:tmp in {
      c.m1(tmp);
      c.m2(tmp);
    }
  }
}
\end{java}
\end{small}
\caption{Fractional permissions using borrowing
and unique references.}
\label{fig:fractional-permissions}
\end{figure}
%
The example in Figure~\ref{fig:fractional-permissions} shows an
implementation of Fractional Permissions. \Joline's borrowing
construct~\cite{wrigstad:2006:phd} is employed to
\emph{temporarily} move a mutable unique reference into an
immutable variable (line 15), freely alias the reference
(while preserving read-only) (lines 16 and 17), and then implicitly move the reference back into
the unique variable again and make it mutable.  This is
essentially Boyland's Fractional Permissions~\cite{Boy03}. Both
owner-polymorphic methods and borrowing blocks guarantee not to
capture the reference. A borrowed reference can be aliased any
number of times in any context to which it has been exported,
without the need to keep track of ``split permissions''
\cite{Boy03} as it is guaranteed that all permissions to alias the
pointer are invalidated when the borrowing block exits. The price
of this convenience is that the conversion from mutable to
immutable and back again must be done in the same place.

Interestingly, \texttt{m1} and \texttt{m2} are equally safe to
call from \texttt{example}. Both methods have revoked their right
to cause write effects to objects owned by \texttt{p}, indicated
by the \JoeImmutable{} and \Read{} annotations on \texttt{p},
respectively. The difference between the two methods is that the
first method knows that \texttt{obj} will not change under foot
(making it safe to, for example, use \texttt{obj} as a key in a
hash table), whereas the second method cannot make such an
assumption.

%%% Local Variables: 
%%% TeX-command-default: "PDF"
%%% End: 

% LocalWords:  contravariant someMethod isIn wildcards ReadOnly readonly Ok tmp
% LocalWords:  Typestates typestates SafeJava Boyland's
